\begin{tabbing}
@$i$ \=Precondition for $a$(Outcome($p$)) \+
\\[0ex]$P$ discrete state(${\it ds}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]c$\wedge$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]$i$;
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = locl($a$))
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}valtype(${\it es}$; $e$); p{-}outcome($p$))\+
\\[0ex]c$\wedge$ ($\uparrow$($P$(es{-}state{-}when(${\it es}$; $e$)))))))
\-\-\\[0ex]$\wedge$ \=(@$i$ discrete ${\it ds}$\+
\\[0ex]$\Rightarrow$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]$i$;
\\[0ex]$e$.existse{-}ge(\=${\it es}$;\+
\\[0ex]$e$;
\\[0ex]${\it e'}$.((es{-}kind(${\it es}$; ${\it e'}$) = locl($a$))
\\[0ex]$\vee$ ($\neg$($\uparrow$($P$(es{-}state{-}after(${\it es}$; ${\it e'}$))))))))
\-\-\\[0ex]$\wedge$ (($\uparrow$($P$(es{-}init{-}state(${\it es}$; $i$)))) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). (loc($e$) = $i$))))))
\-\-\-\-
\end{tabbing}